\begin{tabbing}
$\vdash$  \=$\forall$$A$, $B$:Type, $P$:($A$$\rightarrow\mathbb{P}$), $d$:($x$:$A$$\rightarrow$Dec($P$($x$))), $f$:(\{$x$:$A$$\mid$ $P$($x$)\} $\rightarrow$$B$).\+
\\[0ex]p{-}lift($d$;$f$) $\in$ $A$$\rightarrow$($B$ + Top)
\-
\end{tabbing}